Require Import AutoSep.
Require Import Malloc.

Fixpoint sll (ls : list W) (p : W) : HProp :=
  match ls with
    | nil => [| p = 0 |]
    | x :: ls' => [| p <> 0 |] * [| freeable p 2 |] * Ex p', (p ==*> x, p') * sll ls' p'
  end%Sep.

Theorem sll_extensional : forall ls (p : W), HProp_extensional (sll ls p).
Proof.
  destruct ls; reflexivity.
Qed.

Hint Immediate sll_extensional.

Theorem nil_fwd : forall ls (p : W), p = 0
  -> sll ls p ===> [| ls = nil |].
Proof.
  destruct ls; sepLemma.
Qed.

Theorem nil_bwd : forall ls (p : W), p = 0
  -> [| ls = nil |] ===> sll ls p.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_fwd : forall ls (p : W), p <> 0 
  -> sll ls p ===> [| freeable p 2 |] * Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p'.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_fwd_non_nil : forall ls (p : W), ls <> nil
  -> sll ls p ===> [| p <> 0 |] * [| freeable p 2 |] * Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p'.
Proof.
  destruct ls; sepLemma.
Qed.

Theorem cons_bwd : forall ls (p : W), p <> 0 -> freeable p 2
  -> (Ex x, Ex ls', [| ls = x :: ls' |] * Ex p', (p ==*> x, p') * sll ls' p') ===> sll ls p.
Proof.
  destruct ls; sepLemma;
    match goal with
      | [ H : _ :: _ = _ :: _ |- _ ] => injection H; sepLemma
    end.
Qed.

Definition is_stack(ls:list W)(p:W) : HProp := ([| p <> 0 |] * [| freeable p 2 |] * Ex l, Ex unused, (p ==*> l, unused) * sll ls l)%Sep.

Lemma stack_fwd : forall ls (p:W), is_stack ls p ===> [| p <> 0 |] * [| freeable p 2 |] * Ex l, Ex unused, (p ==*> l,unused) * sll ls l.
Proof.
  unfold is_stack.
  sepLemma.
Qed.

Lemma stack_bwd : forall ls (p:W), p <> 0 -> freeable p 2 -> (Ex l, Ex unused, (p ==*> l,unused) * sll ls l) ===> is_stack ls p.
Proof.
  unfold is_stack.
  sepLemma.
Qed.

Theorem stack_nil_bwd : forall (p:W), p <> 0 -> freeable p 2 -> 
  (Ex unused, p ==*> $0, unused) ===> is_stack nil p.
Proof.
  unfold is_stack.
  sepLemma.
Qed.

Definition hints : TacPackage.
  prepare (nil_fwd, cons_fwd, cons_fwd_non_nil, stack_fwd) (nil_bwd, cons_bwd, stack_bwd
    , stack_nil_bwd).
Defined.

Definition pushS := SPEC("s", "a") reserving 10
  Ex ls,
  PRE[V] is_stack ls (V "s") * mallocHeap
  POST[_] is_stack ((V "a")::ls) (V "s") * mallocHeap.

Definition popS := SPEC("s") reserving 10
  Ex ls,
  PRE[V] is_stack ls (V "s") * [| ls <> nil |] * mallocHeap
  POST[_] is_stack (tl ls) (V "s") * mallocHeap.

Definition createS := SPEC reserving 10
  PRE[V] mallocHeap
  POST[R] is_stack nil R * mallocHeap.

Set Implicit Arguments.

Definition is_empty (A : Type)(ls : list A) : W :=
  match ls with
    | nil => $1
    | _ => $0
  end.

Lemma is_empty_0: forall(A:Type)(ls:list A), is_empty ls = 0 -> ls <> nil.
  intros.
  destruct ls.
  inversion H.
  intuition.
Qed.

Lemma is_empty_1 : forall(A:Type)(ls:list A), is_empty ls <> 0 -> ls = nil.
  intros.
  destruct ls; intuition.
Qed.

Definition is_emptyS := SPEC("s") reserving 5
  Ex ls,
  PRE[V] is_stack ls (V "s")
  POST[R] is_stack ls (V "s") * [| R = is_empty ls |].

Definition destroyS := SPEC("s") reserving 20
  Ex ls,
  PRE[V] is_stack ls (V "s") * mallocHeap
  POST[_] mallocHeap.

Definition stack := bimport [[ "malloc"!"malloc" @ [mallocS], "malloc"!"free" @ [freeS] ]]
bmodule "stack" {{
  bfunction "push"("s", "a", "buf", "ls_head") [pushS]
    "buf" <-- Call "malloc"!"malloc"(0)
    [ Ex ls,
      PRE[V, R] [|R <> 0 |] * [| freeable R 2 |] * R =?> 2 * is_stack ls (V "s")
      POST[_] is_stack ((V "a")::ls) (V "s")];;
    "ls_head" <-* "s";;
    "buf" *<- "a";;
    "buf" <- "buf" + 4;;
    "buf" *<- "ls_head";;
    "buf" <- "buf" - 4;;
    "s" *<- "buf";;
    Return 0
  end with
  bfunction "pop"("s", "ls_head", "old_ls_head") [popS]
    "ls_head" <-* "s";;
    "old_ls_head" <- "ls_head";;
    "ls_head" <-* "ls_head" + 4;;
    "s" *<- "ls_head";;
    Call "malloc"!"free"("old_ls_head", 0)
    [PRE[_,_] Emp
     POST[_] Emp];;
    Return 0
  end with
  bfunction "create"("buf") [createS]
    "buf" <-- Call "malloc"!"malloc"(0)
    [PRE[_,R] [| R <> 0 |] * [| freeable R 2 |] * R =?> 2
     POST[R'] [| R' = R |] * is_stack nil R'];;
    "buf" *<- 0;;
    Return "buf"
  end with
  bfunction "is_empty"("s", "ls_head", "ret") [is_emptyS]
    "ls_head" <-* "s";;
    If ("ls_head" = 0){
      "ret" <- 1
    } else {
      "ret" <- 0
    };;
    Return "ret"
  end with
  bfunction "destroy"("s", "is_emp") [destroyS]
    "is_emp" <-- Call "stack"!"is_empty"("s")
    [ Ex ls,
      PRE[V,R] is_stack ls (V "s") * [| R = is_empty ls |] * mallocHeap
      POST[_] mallocHeap];;
    [Ex ls,
     PRE[V] is_stack ls (V "s") * [| V "is_emp" = is_empty ls |] * mallocHeap
     POST[_] mallocHeap]
    While ("is_emp" = 0){
      Call "stack"!"pop"("s")
      [Ex ls,
       PRE[V,_] is_stack ls (V "s") * mallocHeap
       POST[_] mallocHeap];;
      "is_emp" <-- Call "stack"!"is_empty"("s")
      [ Ex ls,
        PRE[V,R] is_stack ls (V "s") * [| R = is_empty ls |] * mallocHeap
        POST[_] mallocHeap]    
    };;
    Call "malloc"!"free"("s", 0)
    [PRE[_,_] Emp
     POST[_] Emp];;
    Return 0
  end
}}.

(*
Definition stack := bimport [[ "malloc"!"malloc" @ [mallocS], "malloc"!"free" @ [freeS] ]]
bmodule "stack" {{
  bfunction "push"("s", "a", "buf", "ls_head") [pushS]
    Diverge
  end with
  bfunction "pop"("s", "ls_head", "old_ls_head") [popS]
    Diverge
  end with
  bfunction "create"("buf") [createS]
    Diverge
  end with
  bfunction "is_empty"("s", "ls_head", "ret") [is_emptyS]
    Diverge
  end with
  bfunction "destroy"("s", "is_emp") [destroyS]
    "is_emp" <-- Call "stack"!"is_empty"("s")
    [ Ex ls,
      PRE[V,R] is_stack ls (V "s") * [| R = is_empty ls |] * mallocHeap
      POST[_] mallocHeap];;
    [Ex ls,
     PRE[V] is_stack ls (V "s") * [| V "is_emp" = is_empty ls |] * mallocHeap
     POST[_] mallocHeap]
    While ("is_emp" = 0){
      Call "stack"!"pop"("s")
      [Ex ls,
       PRE[V,_] is_stack ls (V "s") * mallocHeap
       POST[_] mallocHeap];;
      "is_emp" <-- Call "stack"!"is_empty"("s")
      [ Ex ls,
        PRE[V,R] is_stack ls (V "s") * [| R = is_empty ls |] * mallocHeap
        POST[_] mallocHeap]    
    };;
    Call "malloc"!"free"("s", 0)
    [PRE[_,_] Emp
     POST[_] Emp];;
    Return 0
  end
}}.
*)

Lemma plus_minus_a : forall n a:W, n = n ^+ a ^- a.
  intros.
  words.
Qed.

Hint Resolve is_empty_0 is_empty_1.
Hint Rewrite <- plus_minus_a : sepFormula.

(*
Hint Extern 1 (@eq W _ _) => words.
*)

Theorem stackOk : moduleOk stack.
Proof.
  vcgen; sep hints; auto.
  words.
Hint Extern 1 (@eq W _ _) => words.
  words.
  words.
  rewrite H5.
  sep hints.
  words.
  rewrite H9.
  rewrite H.
  reflexivity.
  rewrite H9.
  rewrite H.
  reflexivity.
  apply is_empty_0.
  rewrite <- H11.
  assumption.
  words.
  rewrite H12.
  rewrite H9.
  rewrite H1.
  words.
  words.
  rewrite H11 in H9.
  apply is_empty_1 in H9.
  rewrite H9.
  sep hints.
Qed.

Print Assumptions stackOk.